ds:x:Id fp Type, da:k:Knd fp Type, snd:msg-spec(ds;da). msg-spec-links(snd)  IdLnk List 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, IdLnk, x:AB(x), x.A(x), 2of(t), 1of(t), msg-item(ds;da;k;l), type List, fpf-domain(f), map(f;as), msg-spec-links(snd), msg-spec(ds;da), Top, x:AB(x), (x  l), {x:A| B(x) }
Lemmas	list-subtype, map wf, l member wf, fpf-domain wf, fpf-trivial-subtype-top, msg-item wf, pi1 wf, pi2 wf, IdLnk wf, Knd wf, fpf wf, Id wf